(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#equal(@x, @y) → #eq(@x, @y)
appendreverse(@toreverse, @sofar) → appendreverse#1(@toreverse, @sofar)
appendreverse#1(::(@a, @as), @sofar) → appendreverse(@as, ::(@a, @sofar))
appendreverse#1(nil, @sofar) → @sofar
bfs(@queue, @futurequeue, @x) → bfs#1(@queue, @futurequeue, @x)
bfs#1(::(@t, @ts), @futurequeue, @x) → bfs#3(@t, @futurequeue, @ts, @x)
bfs#1(nil, @futurequeue, @x) → bfs#2(@futurequeue, @x)
bfs#2(::(@t, @ts), @x) → bfs(reverse(::(@t, @ts)), nil, @x)
bfs#2(nil, @x) → leaf
bfs#3(leaf, @futurequeue, @ts, @x) → bfs(@ts, @futurequeue, @x)
bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) → bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)
bfs#4(#false, @futurequeue, @t1, @t2, @ts, @x, @y) → bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)
bfs#4(#true, @futurequeue, @t1, @t2, @ts, @x, @y) → node(@y, @t1, @t2)
bfs2(@t, @x) → bfs2#1(dobfs(@t, @x), @x)
bfs2#1(@t', @x) → dobfs(@t', @x)
dfs(@queue, @x) → dfs#1(@queue, @x)
dfs#1(::(@t, @ts), @x) → dfs#2(@t, @t, @ts, @x)
dfs#1(nil, @x) → leaf
dfs#2(leaf, @t, @ts, @x) → dfs(@ts, @x)
dfs#2(node(@a, @t1, @t2), @t, @ts, @x) → dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)
dfs#3(#false, @t, @t1, @t2, @ts, @x) → dfs(::(@t1, ::(@t2, @ts)), @x)
dfs#3(#true, @t, @t1, @t2, @ts, @x) → @t
dobfs(@t, @x) → bfs(::(@t, nil), nil, @x)
dodfs(@t, @x) → dfs(::(@t, nil), @x)
reverse(@xs) → appendreverse(@xs, nil)
The (relative) TRS S consists of the following rules:
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), leaf) → #false
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) → #false
#eq(leaf, ::(@y_1, @y_2)) → #false
#eq(leaf, leaf) → #true
#eq(leaf, nil) → #false
#eq(leaf, node(@y_1, @y_2, @y_3)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, leaf) → #false
#eq(nil, nil) → #true
#eq(nil, node(@y_1, @y_2, @y_3)) → #false
#eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) → #false
#eq(node(@x_1, @x_2, @x_3), leaf) → #false
#eq(node(@x_1, @x_2, @x_3), nil) → #false
#eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) → #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
appendreverse(::(@a4229_5, @as4230_5), @sofar) →+ appendreverse(@as4230_5, ::(@a4229_5, @sofar))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [@as4230_5 / ::(@a4229_5, @as4230_5)].
The result substitution is [@sofar / ::(@a4229_5, @sofar)].
(2) BOUNDS(n^1, INF)